(* -*-sml-*- *)
(*****************************************************************************)
(* Executing f abort b                                                       *)
(* Not for compiling.                                                        *)
(*****************************************************************************)

loadPath := "../official-semantics" :: "../regexp" :: !loadPath;
app 
 load 
 ["bossLib","metisLib","intLib","stringLib","pred_setLib",
  "regexpLib","ExecuteSemanticsTheory","PropertiesTheory"];

quietdec := true;
open bossLib metisLib intLib stringLib rich_listTheory
open regexpLib FinitePSLPathTheory UnclockedSemanticsTheory 
     PropertiesTheory ExecuteSemanticsTheory;
quietdec := false;

(******************************************************************************
* Set the trace level of the regular expression library:      
* 0: silent
* 1: 1 character (either - or +) for each list element processed
* 2: matches as they are discovered
* 3: transitions as they are calculated
* 4: internal state of the automata
******************************************************************************)
set_trace "regexpTools" 1;

(******************************************************************************
* Set default parsing to natural numbers rather than integers 
******************************************************************************)
val _ = intLib.deprecate_int();

(******************************************************************************
* Version of Define that doesn't add to the EVAL compset
******************************************************************************)
val pureDefine = with_flag (computeLib.auto_import_definitions, false) Define;

(******************************************************************************
* For simplification during symbolic evaluation of Sugar2 formulas
******************************************************************************)

val EXISTS_COND = prove
  (``!p c a b.
       EXISTS p (if c then a else b) = if c then EXISTS p a else EXISTS p b``,
   RW_TAC std_ss []);

val COND_SIMP = prove
  (``!c a b.
       (COND c a F = c /\ a) /\ (COND c a T = ~c \/ a) /\
       (COND c T b = c \/ b) /\ (COND c F b = ~c /\ b)``,
   RW_TAC std_ss [IMP_DISJ_THM]);

(******************************************************************************
* Evaluating Sugar2 formulas
******************************************************************************)
val _ = computeLib.add_funs
         ([pred_setTheory.IN_INSERT,
           pred_setTheory.NOT_IN_EMPTY,
           EXISTS_COND, 
           COND_SIMP,
           PSLPathTheory.SEL_REC_AUX,
           UF_SEM_F_UNTIL_REC,
           B_SEM,
           EVAL_US_SEM,
           EVAL_UF_SEM_F_SUFFIX_IMP,
           UF_SEM_F_STRONG_IMP_F_SUFFIX_IMP,
           S_CLOCK_COMP_ELIM,
           F_TRUE_CLOCK_COMP_ELIM,
           DECIDE ``SUC n > 0 = T``]);


(******************************************************************************
* f1 before f2 = [not f2 W (f1 & not f2)]
******************************************************************************)
val F_BEFORE_def =
 Define
  `F_BEFORE(f1,f2) = F_W(F_NOT f2, F_AND(f1, F_NOT f2))`;

(******************************************************************************
* Make ";;" into an infix for S_CAT
******************************************************************************)
val _ = set_fixity ";;" (Infixl 500);
val S_CAT_IX_def = xDefine "S_CAT_IX" `$;; r1 r2 = S_CAT(r1,r2)`;

(******************************************************************************
* Make "->" into an infix for F_IMPLIES
******************************************************************************)
val _ = set_fixity "->" (Infixl 600);
val F_IMPLIES_IX_def = xDefine "F_IMPLIES_IX" `$-> f1 f2 = F_IMPLIES(f1,f2)`;

(******************************************************************************
* Make "until" into an infix for F_W
******************************************************************************)
val _ = set_fixity "until" (Infixl 440);
val until_IX_def = xDefine "until_IX" `$until f1 f2 = F_W(f1,f2)`;

(******************************************************************************
* Make "abort" into an infix for F_ABORT
******************************************************************************)
val _ = set_fixity "abort" (Infixl 445);
val abort_IX_def = xDefine "abort_IX" `$abort f b = F_ABORT(f,b)`;

(******************************************************************************
* eventually!
******************************************************************************)
val eventually_bang_def = Define `eventually_bang = F_F`;

(******************************************************************************
* always
******************************************************************************)
val always_def = Define `always = F_G`;


(******************************************************************************
* Fig. 8, page 22, from Sugar 2.0 Accellera Submission
*
* time       00  01  02  03  04  05  06  07  08  09  10  11  12  13  14  17
* -------------------------------------------------------------------------
* start      0   1   1   0   0   0   0   0   0   0   0   0   0   0   0   0
* req        0   0   0   1   1   0   0   1   1   0   0   0   1   1   0   0
* ack        0   0   0   0   0   1   1   0   0   0   0   0   0   0   0   0
* interrupt  0   0   0   0   0   0   0   0   0   0   1   1   0   0   0   0
******************************************************************************)

val prop_defs =
 [Define `start     = 0`,
  Define `req       = 1`,
  Define `ack       = 2`,
  Define `interrupt = 3`];

val Fig8_def =
 Define
 (*        0  1       2       3     4     5     6     7     8     9  *)
  `Fig8 = [{};{start};{start};{req};{req};{ack};{ack};{req};{req};{};
 (*        10          11          12    13    14 15                 *)
           {interrupt};{interrupt};{req};{req};{};{}]`;


val UF_SEM_Fig8_abort =
 time
  EVAL
  ``UF_SEM
     (FINITE Fig8)
     (always
      (F_BOOL(B_PROP start)
       ->
       ((F_BOOL(B_PROP req) -> eventually_bang (F_BOOL(B_PROP ack)))
        abort
        (B_PROP interrupt))))``;

val UF_SEM_Fig8_until =
 time
  EVAL
  ``UF_SEM
     (FINITE Fig8)
     (always
      (F_BOOL(B_PROP start)
       ->
       ((F_BOOL(B_PROP req) -> eventually_bang (F_BOOL(B_PROP ack)))
        until
        (F_BOOL(B_PROP interrupt)))))``;

val F_SEM_Fig8_abort =
 time
  EVAL
  ``F_SEM
     (FINITE Fig8)
     B_TRUE
     (always
      (F_BOOL(B_PROP start)
       ->
       ((F_BOOL(B_PROP req) -> eventually_bang (F_BOOL(B_PROP ack)))
        abort
        (B_PROP interrupt))))``;

val F_SEM_Fig8_until =
 time
  EVAL
  ``F_SEM
     (FINITE Fig8)
     B_TRUE
     (always
      (F_BOOL(B_PROP start)
       ->
       ((F_BOOL(B_PROP req) -> eventually_bang (F_BOOL(B_PROP ack)))
        until
        (F_BOOL(B_PROP interrupt)))))``;
